Skip to content

[TRACK_B] Close the keselamatan family (41/42), and fix two divergences it exposed - #74

Merged
ib823 merged 3 commits into
mainfrom
claude/continue-solution-4gn31y
Aug 20, 2026
Merged

[TRACK_B] Close the keselamatan family (41/42), and fix two divergences it exposed#74
ib823 merged 3 commits into
mainfrom
claude/continue-solution-4gn31y

Conversation

@ib823

@ib823 ib823 commented Aug 20, 2026

Copy link
Copy Markdown
Owner

REQ-70. Routes the remaining 17 security builtins, taking the family from 24/42 to 41/42. Getting there required fixing two divergences in families the plan had already marked closed — both invisible to the differentials those families shipped with, and both prerequisites rather than side quests.

The deferral was wrong, and checking it is what unblocked this

The previous increment routed only the single-argument subset, reasoning that eleven members take a pair and split_pair hands back a Value::BuiltinPartial for a non-pair argument, which the C backend has no equivalent of.

That reasoning does not hold. Every one of those signatures is typed Ty::Prod(..) -> _ in riina-typechecker, so the curried form f(a, b) is rejected at type-check, identically under riinac run and riinac build, and only f((a, b)) ever reaches a runtime. The interpreter's partial arm is unreachable from well-typed source, so C needing no partial-application machinery costs nothing. A test pins that, because it is the assumption eleven C implementations rest on.

Prerequisite 1 — the C JSON parser could not fail

riina_json_parse_value had no error path at all: unknown input fell through to strtoll and became a value. Five classes, each silent:

input riinac run compiled binary
xyz unexpected char 'x' 0
(empty) unexpected end of input 0
12abc unexpected trailing content 12
nul expected 'null' ()
[1,2 expected ',' or ']' in array [1,2]

A compiled program parsing attacker-controlled JSON saw a fabricated value where the interpreter refuses. json_differential missed it because all nine of its cases fed well-formed input, so a parser that cannot fail was never asked to. And json_parse_safe/nyahsiri_selamat could not be routed at all: their whole contract is "malformed input yields Unit", and "malformed" had no meaning on the C side.

The parser now mirrors builtins/json.rs production-for-production, including the parts that are not obviously deliberate: whitespace is Unicode (str::trim), not the ASCII four; a lone surrogate in a \uXXXX escape decodes to nothing (char::from_u32 is None and the interpreter pushes no character); and a number is read as u64 first, then as f64 with Rust's saturating as u64 cast — so -5 is 0, where strtoll plus a C cast gave 18446744073709551611.

Prerequisite 2 — composite values rendered as the literal text <value>

riina_format handled the scalar tags and defaulted every composite one — PAIR, LIST, MAP and both SUM arms — to "<value>". cetakln and ke_teks both go through it, so a compiled program printing a list showed <value> where riinac run shows [1, 2, 3].

That also made sahkan_panjang unroutable in practice: it returns an Option, so its answer was unobservable in compiled code — the REQ-79 "compiles but you cannot see the result" trap in a new costume. ke_teks additionally carried its own copy of the scalar arms, which is how the two came to disagree; it now delegates, so there is one switch rather than two.

The interpreter has two rendering modes that spell values differently: builtins::format_value prints a string bare and a bool as betul/salah, while Value's Display — which format_value falls through to, and which is the only path a sum takes — quotes the string and prints Rust's English true/false. So the same bool is betul in a list and true in a sum. That is an inconsistency in the reference, not a design, but the reference is what a compiled program must match; both modes are mirrored rather than tidied, and pinned so that changing it is a language decision and not codegen drift.

Routed

Seven pair-taking modelled sinks (dom_set_html/attr, email_send/set_header, http_post/put/delete), validate_length, the three CSRF predicates, the safe-file trio, and the three safe parsers.

The safe-file trio share the verified gate with fail_* — the interpreter calls the same fail::gate_read/gate_write/gate_delete — so the emitted C reaches the same riina_gate. A "safe" file op that skipped the access check would be the REQ-72 bypass wearing the word selamat. They were routable only because the gate landed in #73.

Not routed, deliberately

csrf_generate/csrf_jana, the single remaining member. Its result is not a function of its input (a token seeded from the clock and a process-local counter), so the backends can be held only to a shape, not to agreement. Mirroring it would mean transcribing Rust's DefaultHasher into C to reproduce a generator its own doc comment already marks as "a reference token, not a certified CSPRNG" — spreading that to a second implementation makes the eventual fix twice the work. Nothing is cut off: csrf_validate takes plain Teks, so a compiled program can carry tokens minted elsewhere, unlike the sanitizers which would have been unreachable without baca_baris.

Recorded, not fixed — a stdlib defect the differential surfaced

sanitasi_json is the only producer of Disanitasi<Teks, JsonValidation> and so the only way to reach json_urai_selamat, but it is a string-embedding escaper: it turns {"a":1} into {\"a\":1}. Every JSON object therefore arrives malformed and parses to Unit, because object keys are quoted; only quote-free documents survive. Both backends agree on this, so it is a type-signature defect in the security stdlib — the gate on a safe parser should be a validation, not an escape — and not a divergence. Pinned in both directions so a fix has to update the test deliberately.

Tests

keselamatan_differential 14 → 24, json_differential 9 → 13, collection_differential 7 → 9.

The keselamatan additions cover the empty allowed-origin arms (a C author reaching for strncmp alone would accept every origin), character-vs-byte length counting, gate parity for the safe-file trio including a denied non-owner write, and the safe parsers on each malformed class.

Verification

  • 03_PROTO: 3360 passing, 0 failed (+30)
  • 05_TOOLING: 323 passing, 0 failed
  • cargo clippy -- -D warnings: clean on both workspaces
  • scripts/audit-docs.sh: 0 discrepancies (2 pre-existing warnings, unrelated: Lean sorry syntactic-only, Coq warning-budget freshness)
  • scripts/update-proof-ledger.sh --check: up to date
  • docs/api/STDLIB.md regenerated from the compiler — counts re-derived, not carried forward: 376 registered, 323 compile (compiled 20 / native-only 303 / interp-only 50)

🤖 Generated with Claude Code

https://claude.ai/code/session_01Uu28z8CdRQ1SLzTv8yszth


Generated by Claude Code

claude added 3 commits August 20, 2026 01:33
… it exposed

REQ-70. Routes the remaining 17 security builtins, taking the family from 24/42
to 41/42. Getting there required fixing two divergences in families the plan had
already marked closed -- both invisible to the differentials those families
shipped with, and both prerequisites rather than side quests.

THE DEFERRAL WAS WRONG, AND CHECKING IT IS WHAT UNBLOCKED THIS. The previous
increment routed only the single-argument subset, reasoning that eleven members
take a pair and split_pair hands back a Value::BuiltinPartial for a non-pair
argument, which the C backend has no equivalent of. That reasoning does not
hold: every one of those signatures is typed Ty::Prod(..) -> _ in
riina-typechecker, so the curried form f(a, b) is REJECTED AT TYPE-CHECK,
identically under `riinac run` and `riinac build`, and only f((a, b)) ever
reaches a runtime. The interpreter's partial arm is unreachable from well-typed
source, so C needing no partial-application machinery costs nothing. A test now
pins that, because it is the assumption the eleven C implementations rest on.

PREREQUISITE 1 -- THE C JSON PARSER COULD NOT FAIL. riina_json_parse_value had
no error path at all: unknown input fell through to strtoll and became a value.
Five classes, each SILENT --

  input     riinac run                       compiled binary
  "xyz"     unexpected char 'x'              0
  ""        unexpected end of input          0
  "12abc"   unexpected trailing content      12
  "nul"     expected 'null'                  ()
  "[1,2"    expected ',' or ']' in array     [1,2]

A compiled program parsing attacker-controlled JSON saw a FABRICATED value where
the interpreter refuses. json_differential missed it because all nine of its
cases fed WELL-FORMED input, so a parser that cannot fail was never asked to.
And json_parse_safe/nyahsiri_selamat could not be routed at all: their whole
contract is "malformed input yields Unit", and "malformed" had no meaning on the
C side.

The parser now mirrors builtins/json.rs production-for-production, including the
parts that are not obviously deliberate: whitespace is UNICODE (str::trim), not
the ASCII four; a lone surrogate in a \uXXXX escape decodes to nothing
(char::from_u32 is None and the interpreter pushes no character); and a number
is read as u64 first, then as f64 with Rust's SATURATING as-u64 cast -- so "-5"
is 0, where strtoll plus a C cast gave 18446744073709551611. Failure is recorded
rather than raised in place, so json_urai can report it and json_parse_safe can
swallow it.

PREREQUISITE 2 -- COMPOSITE VALUES RENDERED AS THE LITERAL TEXT <value>.
riina_format handled the scalar tags and defaulted every composite one -- PAIR,
LIST, MAP and both SUM arms -- to "<value>". cetakln and ke_teks both go through
it, so a compiled program printing a list showed <value> where riinac run shows
[1, 2, 3]. That also made sahkan_panjang unroutable in practice: it returns an
Option, so its answer was unobservable in compiled code -- lowering it would
have been the REQ-79 "compiles but you cannot see the result" trap. ke_teks
additionally carried its own COPY of the scalar arms, which is how the two came
to disagree; it now delegates, so there is one switch rather than two.

The interpreter has two rendering modes that spell values differently:
builtins::format_value prints a string bare and a bool as betul/salah, while
Value's Display -- which format_value falls through to, and which is the ONLY
path a sum takes -- quotes the string and prints Rust's English true/false. So
the same bool is betul in a list and true in a sum. That is an inconsistency in
the reference, not a design, but the reference is what a compiled program must
match; both modes are mirrored rather than tidied, and pinned so that changing
it is a language decision and not codegen drift.

ROUTED: seven pair-taking modelled sinks (dom_set_html/attr, email_send/
set_header, http_post/put/delete), validate_length, the three CSRF predicates,
the safe-file trio, and the three safe parsers.

The safe-file trio share the VERIFIED GATE with fail_* -- the interpreter calls
the same fail::gate_read/gate_write/gate_delete -- so the emitted C reaches the
same riina_gate. A "safe" file op that skipped the access check would be the
REQ-72 bypass wearing the word `selamat`. They were routable only because the
gate landed in #73.

NOT ROUTED: csrf_generate/csrf_jana, the single remaining member. Its result is
not a function of its input (a token seeded from the clock and a process-local
counter), so the backends cannot be held to agreement by a differential, only to
a shape. Mirroring it would mean transcribing Rust's DefaultHasher into C to
reproduce a generator its own doc comment already marks as "a *reference* token,
not a certified CSPRNG" -- spreading that to a second implementation makes the
eventual fix twice the work. Nothing is cut off: csrf_validate takes plain Teks,
so a compiled program can carry tokens minted elsewhere, unlike the sanitizers
which would have been unreachable without baca_baris.

RECORDED, NOT FIXED -- a stdlib defect the differential surfaced.
sanitasi_json is the only producer of Disanitasi<Teks, JsonValidation> and so
the only way to reach json_urai_selamat, but it is a string-EMBEDDING escaper:
it turns {"a":1} into {\"a\":1}. Every JSON object therefore arrives malformed
and parses to Unit, because object keys are quoted; only quote-free documents
survive. Both backends agree on this, so it is a type-signature defect in the
security stdlib -- the gate on a safe PARSER should be a validation, not an
escape -- and not a divergence. Pinned in both directions so a fix has to update
the test deliberately.

Tests: keselamatan_differential 14 -> 24, json_differential 9 -> 13,
collection_differential 7 -> 9. The keselamatan additions cover the empty
allowed-origin arms (a C author reaching for strncmp alone would accept every
origin), character-vs-byte length counting, gate parity for the safe-file trio
including a denied non-owner write, and the safe parsers on each malformed
class.

Verified: 03_PROTO 3360/0 (+30), 05_TOOLING 323/0, clippy clean on both,
audit-docs.sh 0 discrepancies. STDLIB.md regenerated from the compiler.
…nces it exposed

Updates the REQ-70 row and the Part 12 Wave 1.0 status. Counts re-derived from
the compiler via docs/api/STDLIB.md rather than carried forward: 376 registered,
323 compile -- compiled 20 / native-only 303 / interp-only 50 (was 218 of 373
at the 2026-08-15 entry).

Records, per Prime Directive 2, the three things this increment established
that are not visible from the diff:

* the previous increment's pair/currying deferral was WRONG -- the typechecker
  rejects the curried form, so no partial-application machinery was ever needed;
* the emitted C JSON parser could not fail, so a compiled program parsing
  attacker-controlled input saw a fabricated value where the interpreter
  refuses, in a family this row already listed as closed;
* sanitasi_json is the only producer of the type json_urai_selamat accepts, but
  it is a string-embedding escaper, so every JSON object arrives malformed --
  a type-signature defect in the security stdlib, agreed on by both backends
  and therefore not a codegen divergence. Recorded, not fixed.

Also generalises the recurring finding now that six families are through it: a
family marked as lowering is not thereby a family that agrees, and neither is a
family with a differential -- json's differential passed nine cases while the C
parser could not reject anything, because every case fed well-formed input.
@ib823
ib823 marked this pull request as ready for review August 20, 2026 09:55
@ib823
ib823 merged commit 2425d75 into main Aug 20, 2026
11 checks passed
ib823 pushed a commit that referenced this pull request Aug 20, 2026
…ests)

The metrics.json carried in #74 was stale: 3330 tests, testsSource
cached_verified, and git.branch naming the feature branch. Regenerated on main
from a full cargo test run -- 3360 / full_cargo_test -- and the Tier 1/2 banners
re-synced from it (47 files).

Per Prime Directive 8 the counts are re-derived by command, never copied:
website/public/metrics.json is the single source of truth and every doc now
agrees with it. audit-docs.sh reports 0 discrepancies; the 2 warnings are
pre-existing and unrelated (Lean sorry count is syntactic-only, Coq
warning-budget freshness).
ib823 pushed a commit that referenced this pull request Aug 20, 2026
Timestamp/commit stamps written by sync-public.sh and deploy-website.sh, plus
the rebuilt website WASM bundle. No behaviour change: metrics.json's counts are
unchanged from the refresh in ec793e0 (3360 tests, full_cargo_test); only
'generated' and git.commit move.
ib823 pushed a commit that referenced this pull request Aug 20, 2026
I recorded 376 registered builtins in the #74 plan update. That count came from
grepping table rows in docs/api/STDLIB.md with a pattern loose enough to also
match the three-row Backend LEGEND. The real total is 373; the 20 / 303 / 50
split was right, and the legend states each of those three numbers itself.

Exactly the drift Prime Directive 8 exists to catch -- a count derived by a
sloppy command is not better than a copied one. Re-derived with a pattern
anchored on the signature cell, and cross-checked against the legend's own
totals (20 + 303 + 50 = 373).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants